7.2. 头部与签名（Headers and Signatures）🔗

定义或声明的头部（若有）由待声明/定义的常量以及其签名组成。常量的签名指定了它可以如何被使用。签名中包含的不仅仅是类型本身的信息，还包括例如宇宙层级参数、可选参数的默认值等。在 Lean 中，不同类型的声明均使用一致的格式来书写签名。

大多数头部以一个 声明名称 开始，随后是其真正的签名：参数列表以及结果类型。一个声明名称可以可选地包含宇宙层级参数。

syntax声明名称

不带宇宙参数的声明名称仅由一个标识符组成：

declId ::=
    `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names ident

带宇宙参数的声明名称由一个标识符，后接一个点与一组花括号中的一个或多个宇宙参数名构成：

declId ::= ...
    | `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names ident.{ident, ident,*}

这些宇宙参数名是绑定出现（binding occurrences）。

示例（example）不包含声明名称；而实例声明（instance）的名字是可选的。

7.2.2. 参数与类型（Parameters and Types）🔗

在（可选的）名字之后，是声明头部的签名部分。签名用于指定声明的参数以及其类型。

syntax声明签名

一个签名由零个或多个参数构成，后跟一个冒号与一个类型：

declSig ::=
    `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole | bracketedBinder)* : term

syntax可选签名

许多情况下签名本身是可选的。这时即便省略类型，也可以仅提供参数：

optDeclSig ::=
    `optDeclSig` matches the signature of a declaration with optional type: a list of binders and then possibly `: type` (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole | bracketedBinder)* (: term)?

参数可以有三种形式：

标识符：为参数命名，但不提供类型。这类参数的类型必须在繁释阶段推断出来。
下划线（_）：表示该参数在局部作用域中不能通过名字访问。这类参数的类型同样需要在繁释阶段推断。
带括号参数（bracketed binder）：可以为一个或多个参数指定所有方面的信息，包括名称、类型、默认值，以及其是显式、隐式、严格隐式或实例隐式。

7.2.3. 带括号参数绑定（Bracketed Parameter Bindings）🔗

除标识符与下划线外的其它参数形式统称为 带括号参数，因为它们的语法形式都使用了某种括号（圆括号、花括号或方括号）。所有带括号参数都会显式给出参数类型，并且多数情况下也会包含参数名。对于“实例隐式”参数，名字是可选的。用下划线（_）替代参数名表示匿名参数。

syntax显式参数

使用圆括号括起的参数表示显式参数。如果提供了多个标识符或下划线，则它们都会成为具有相同类型的多个参数：

bracketedBinder ::=
    Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
((ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole) (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term)

syntax可选与自动参数

带有 := 的圆括号参数用于为参数指定默认值。带默认值的参数称为 可选参数。在调用位置，如果未提供该参数，则会使用给定的默认项进行填充。签名中之前的参数在默认值表达式内可见，且其在调用点的实参会被替换进默认值表达式。

如果提供了一个策略脚本，则会在调用点执行该脚本以合成一个参数值；通过策略填充的参数称为 自动参数。

bracketedBinder ::= ...
    | Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
((ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole) (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term := term)

syntax隐式参数

使用花括号的参数表示隐式参数。除非在调用点以名字显式提供，否则它们预期将通过统一过程在调用点被自动合成。隐式参数会在所有调用点尝试合成：

bracketedBinder ::= ...
    | Implicit binder, like `{x y : A}` or `{x y}`.
In regular applications, whenever all parameters before it have been specified,
then a `_` placeholder is automatically inserted for this parameter.
Implicit parameters should be able to be determined from the other arguments and the return type
by unification.

In `@` explicit mode, implicit binders behave like explicit binders.
{(ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole) (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term}

syntax严格隐式参数

使用双层花括号的参数表示严格隐式参数。 ⦃ … ⦄ 与 {{ … }} 等价。和隐式参数类似，若未以名字提供，它们预期通过统一在调用点被合成。严格隐式参数仅当签名中其后的后续参数也被提供时才会尝试在调用点合成。

bracketedBinder ::= ...
    | Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
a `_` placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.

Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.
⦃(ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole) (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term⦄

bracketedBinder ::= ...
    | Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
a `_` placeholder until at least one subsequent explicit parameter is specified.
Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.

Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
and `h hs` has type `p y`.
In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
with `?m` a fresh metavariable.
{{(ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole) (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term}}

syntax实例隐式参数

使用方括号的参数表示实例隐式参数，它们会在调用点通过实例合成被推导：

bracketedBinder ::= ...
    | Instance-implicit binder, like `[C]` or `[inst : C]`.
In regular applications without `@` explicit mode, it is automatically inserted
and solved for by typeclass inference for the specified class `C`.
In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
[(ident :)? term]

这些参数在签名的类型（位于冒号之后）中总是处于作用域内。它们同样在声明的主体中可见；而由类型内部绑定的名字仅在类型内部可见。因此，参数名通常会被使用两次：

作为声明函数类型中的名字，作为依值函数类型的一部分被绑定；
作为声明主体中的名字。在函数定义里，它们由 Lean.Parser.Term.fun : termfun 进行绑定。

参数作用域（Parameter Scope）

add 的签名包含一个参数 n。此外，签名的类型为 (k : Nat) → Nat，这是一个包含 k 的函数类型。参数 n 在函数体内处于作用域中，而 k 不在。

def add (n : Nat) : (k : Nat) → Nat
  | 0 => n
  | k' + 1 => 1 + add n k'

与 add 类似，mustBeEqual 的签名也包含一个参数 n。它既在类型中可见（该类型中的命题涉及到它），也在定义体中可见（作为消息的一部分出现）。

def mustBeEqual (n : Nat) : (k : Nat) → n = k → String :=
  fun _ =>
    fun
    | rfl => s!"Equal - both are {n}!"

关于函数应用的章节函数应用详细说明了可选、自动、隐式与实例隐式等参数的解释规则。

7.2.4. 自动隐式参数（Automatic Implicit Parameters）🔗

默认情况下，出现在签名中的未绑定名字在可行时会被转换为隐式参数。这些参数称为 自动隐式参数。当这些名字不处于函数应用的函数位置，且签名中有足够信息可以推断其类型以及关于它们的顺序约束时，这种转换是可行的。该过程会迭代进行：如果为新插入的隐式参数所推断的类型包含尚未唯一确定的依赖项，则这些依赖会被进一步的隐式参数所替换。

不对应于签名中书写之名字的隐式参数会被分配类似于证明中不可触达假设的名字，这些名字无法被引用。它们会以带有尾随短剑符号（✝）的形式出现在签名里。这样可以避免 Lean 任意选择的名字经由具名参数成为 API 的一部分。

自动隐式参数（Automatic Implicit Parameters）

在下面对 map 的定义中，α 与 β 并未显式绑定。这不会报错，而是会被转换为隐式参数。由于它们必须是类型，且其宇宙层级未受任何约束，因此还会自动插入宇宙层级参数 u 与 v：

def map (f : α → β) : (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs

map 的完整签名为：

map.{u, v} {α : Type u} {β : Type v}
  (f : α → β) (xs : List α) :
  List β

无自动隐式参数（No Automatic Implicit Parameters）

在这个定义中，α 与 β 没有被显式绑定。由于禁用了 autoImplicit，这会导致错误：

set_option autoImplicit false

def map (f : unknown identifier 'α'α → unknown identifier 'β'β) : (xs : List unknown identifier 'α'α) → List unknown identifier 'β'β
  | [] => []
  | x :: xs => f x :: map f xs

unknown identifier 'α'

unknown identifier 'β'

给出完整签名即可通过：

set_option autoImplicit false

def map.{u, v} {α : Type u} {β : Type v}
    (f : α → β) :
    (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs

对于未显式标注类型的参数，其宇宙参数会被自动插入。即便禁用了 autoImplicit，类型参数所处的宇宙也可被推断，并插入相应的宇宙参数：

set_option autoImplicit false

def map {α β} (f : α → β) :
    (xs : List α) → List β
  | [] => []
  | x :: xs => f x :: map f xs

多轮自动隐式参数（Iterated Automatic Implicit Parameters）

给定一个以上界 n（类型 Fin n）约束的数，一个 AtLeast i 表示一个自然数以及它不少于 i 的证明。

structure AtLeast (i : Fin n) where
  val : Nat
  val_gt_i : val ≥ i.val

这些数可以相加：

def AtLeast.add (x y : AtLeast i) : AtLeast i :=
  AtLeast.mk (x.val + y.val) <| byn✝:Nati:Fin n✝x:AtLeast iy:AtLeast i⊢ x.val + y.val ≥ ↑i
    cases xmkn✝:Nati:Fin n✝y:AtLeast ival✝:Natval_gt_i✝:val✝ ≥ ↑i⊢ { val := val✝, val_gt_i := val_gt_i✝ }.val + y.val ≥ ↑i
    cases ymk.mkn✝:Nati:Fin n✝val✝¹:Natval_gt_i✝¹:val✝¹ ≥ ↑ival✝:Natval_gt_i✝:val✝ ≥ ↑i⊢ { val := val✝¹, val_gt_i := val_gt_i✝¹ }.val + { val := val✝, val_gt_i := val_gt_i✝ }.val ≥ ↑i
    dsimp onlymk.mkn✝:Nati:Fin n✝val✝¹:Natval_gt_i✝¹:val✝¹ ≥ ↑ival✝:Natval_gt_i✝:val✝ ≥ ↑i⊢ val✝¹ + val✝ ≥ ↑i
    omegaAll goals completed! 🐙

AtLeast.add 的签名需要多轮自动隐式参数插入。首先插入 i；但它的类型依赖于 Fin n 的上界 n。第二轮插入 n（名字由系统选择）。由于 n 的类型为 Nat，没有进一步依赖，过程终止。可以用 Lean.Parser.Command.check : command#check 查看最终签名：

AtLeast.add {n✝ : Nat} {i : Fin n✝} (x y : AtLeast i) : AtLeast i#check AtLeast.add

AtLeast.add {n✝ : Nat} {i : Fin n✝} (x y : AtLeast i) : AtLeast i

由于 section variables 引入的参数会先被插入，自动隐式参数的插入发生在其之后。与节变量对应的参数即便并未直接对应于签名中书写的某个名字，仍会与其对应的节变量同名；而禁用自动隐式参数对这些对应于节变量的参数不起作用。不过，当启用自动隐式参数时，包含其他未绑定变量的节变量声明还会获得遵循与隐式参数相同规则的附加节变量。

自动隐式参数的插入由两个选项控制。默认情况下，该插入处于“宽松（relaxed）”模式，这意味着任何未绑定的标识符都可能成为自动插入的候选。将 relaxedAutoImplicit 设为 false 会禁用宽松模式，此时仅由“单个字母后跟零个或多个数字”构成的标识符才会被考虑用于自动插入。

option

relaxedAutoImplicit

Default value: true

When "relaxed" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see option autoImplicit).

option

autoImplicit

Default value: true

Unbound local variables in declaration headers become implicit arguments. In "relaxed" mode (default), any atomic identifier is eligible, otherwise only single character followed by numeric digits are eligible. For example, def f (x : Vector α n) : Vector α n := automatically introduces the implicit variables {α n}.

宽松 vs 非宽松的自动隐式参数（Relaxed vs Non-Relaxed Automatic Implicit Parameters）

拼写错误的标识符或缺失的导入，可能会变成意外的隐式参数，如下例所示：

inductive Answer where
  | yes
  | maybe
  | no

def select (choices : α × α × α) : Asnwer →  α
  | invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  Asnwer.yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2

报错信息指出参数的类型不是常量，因此不能在模式中使用点记法：

invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
  Asnwer

原因是其签名为：

select.{u_1, u_2}
  {α : Type u_1}
  {Asnwer : Sort u_2}
  (choices : α × α × α) :
  Asnwer → α

禁用“宽松”的自动隐式参数后，错误更清晰，同时仍允许自动插入类型：

set_option relaxedAutoImplicit false

def select (choices : α × α × α) : unknown identifier 'Asnwer'Asnwer →  α
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2

unknown identifier 'Asnwer'

修正该错误后，定义即可通过：

set_option relaxedAutoImplicit false

def select (choices : α × α × α) : Answer →  α
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2

完全关闭自动隐式参数会导致该定义被拒绝：

set_option autoImplicit false

def select (choices : unknown identifier 'α'α × unknown identifier 'α'α × unknown identifier 'α'α) : Answer →  unknown identifier 'α'α
  | .yes => choices.1
  | .maybe => choices.2.1
  | .no => choices.2.2

unknown identifier 'α'

Lean 语言参考手册

7.2. 头部与签名（Headers and Signatures）🔗

7.2.1. 声明名称（Declaration Names）

7.2.2. 参数与类型（Parameters and Types）🔗

7.2.3. 带括号参数绑定（Bracketed Parameter Bindings）🔗

7.2.4. 自动隐式参数（Automatic Implicit Parameters）🔗